nLab homotopy theory in homotopy type theory -- references

Homotopy theory formalized in homotopy type theory

Homotopy theory formalized in homotopy type theory

The following is a list of topics and results of homotopy theory that have been formalized in homotopy type theory.


On homotopy groups of spheres:

On Whitehead's theorem:

On Eilenberg-MacLane spaces:

On ordinary cohomology:

On the Freudenthal suspension theorem:

  • Implies π k(S n)=π k+1(S n+1)\pi_k(S^n) = \pi_{k+1}(S^{n+1}) whenever k2n2k \leq 2n - 2

  • Peter’s encode/decode-style proof, formalized by Dan, using a clever lemma about maps out of 2 n-connected types. This is the “95%” version, which shows that the relevant map is an equivalence on truncations.

  • The full “100%” version, formalized by Dan, which shows that the relevant map is 2n2n-connected.

On homotopy limits:

  • Jeremy Avigad, Chris Kapulkin and Peter Lumsdaine arXiv Coq code

On the van Kampen theorem:

On covering spaces:

  • Favonia’s proofs (link in flux due to library rewrite).

On Blakers-Massey theorem:

  • Favonia/Peter/Guillaume/Dan’s formalization of Peter/Eric/Dan’s proof (link in flux due to library rewrite).

Created on June 9, 2022 at 07:13:54. See the history of this page for a list of all contributions to it.